const fs = require("fs");
const { processTimeDetailInfo } = require("./time_detail");

function readFileAsString(filePath) {
  return new Promise((resolve, reject) => {
    fs.readFile(filePath, "utf8", (err, data) => {
      if (err) {
        if (err.errno === -2) {
          resolve({ data: null });
        }
        reject(err);
        return;
      }
      resolve({ data });
    });
  });
}

const capitalizedOnlyFirst = (word) =>
  word.charAt(0).toUpperCase() + word.slice(1).toLowerCase();

function process_ltlfsyn(data) {
  const match = data.match(/^(Unrealizable|Realizable)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/Unrealizable|Realizable/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

// function process_ltlfsynSyft(data) {
//   // console.log(data)
//   // throw new Error();
//   const match = data.match(/^(Unrealizable|Realizable)/)
//     || data.match(/Total CPU time used in synthesis: \d+ ms\n(Unrealizable|Realizable)/);
//   if (match) {
//     return {
//       result: capitalizedOnlyFirst(
//         match[0].match(/Unrealizable|Realizable/)[0]
//       ),
//     };
//   } else {
//     return {
//       result: "Stopped",
//     };
//   }
// }

function getMatchResFor_Combine01(lines, syn_res)
{
  let matchLogLine = null;
  // console.log(lines);
  // throw new Error("NotImplemented");
  for (let i = lines.length - 1; i >= 0; i--)
  {
    const lineStr = lines[i];
    matchLogLine = lineStr.match(/return Realizable after PreCheck!$/);
    let breakFlag = true;
    let matchRaw_arr = null;
    if (matchRaw_arr = lineStr.match(/return (Realizable|Unrealizable) after PreCheck!$/)) {
      // console.log(matchRaw_arr);
      matchLogLine = "PreCheck-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^PreCheck synthesis return (Realizable|Unrealizable)!$/)) {
      // console.log(matchRaw_arr);
      matchLogLine = "PreCheck-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/::Group::	SearchWholeDFA \(sub_af in sysGroup\) return (Realizable|Unrealizable)!/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^::Group::	Finish syft_check_DFA_realizability return (Realizable|Unrealizable)$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^Finish syft_check_DFA_realizability return (Realizable|Unrealizable)$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^compositional_synthesis return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^Backward synthesis return (Realizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + matchRaw_arr[1]
    }
    else if (matchRaw_arr = lineStr.match(/^SearchWholeDFA return (Realizable|unrealizable|Unrealizable)!$/)) {
      matchLogLine = "DFA-" + capitalizedOnlyFirst(matchRaw_arr[1])
    }
    else {
      breakFlag = false;
    }
    if (breakFlag)
        break;
  }
  if (!matchLogLine)
    {
      return "NoLog-" + syn_res;
    }
  if (matchLogLine.substring(matchLogLine.length-syn_res.length) != syn_res)
    {
      console.log(matchLogLine, syn_res);
    return "ERROR";
    }
  return matchLogLine;
}

function process_ltlfsynSyft(data) {
  let match = null;
  const lines = data.split('\n');
  // for (let i = 0; i < lines.length; i++)
  let timout_exited_line_idx = null;
  for (let i = lines.length - 25; i >= 0; i--)
  {
    const lineStr = lines[i];
    match = lineStr.match(/^(Unrealizable|Realizable)$/);
    if (match) {
      // console.log(lineStr);
      break;
    }
    if (timout_exited_line_idx != null)
        break;
    if (lineStr.match(/^(Command exited with non-zero status)/)) {
      timout_exited_line_idx = i;
    }
  }
  if (match) {
    const syn_res = match[0].match(/Unrealizable|Realizable/)[0];
    return {
      result: syn_res,
      resultType: capitalizedOnlyFirst(
        syn_res
      ),
    };
  } else {
    return {
      result: "Stopped",
      resultType: "Stopped",
    };
  }
}

function process_ltlfsynSyft_Cases(data) {
  if (!data.includes('Command being timed'))
  {
    return {
      result: "Running",
      resultType: "Running",     
    }
  }
  const lines = data.split('\n');
  if (lines[0].startsWith("+ /usr/bin/time"))
    lines.splice(0, 1);
  const timeoutLines = lines.slice(lines.length - 24);
  const reducedLines = lines.slice(0, lines.length - 24);
  const syn_res_str = reducedLines[reducedLines.length - 1];
  const match = syn_res_str.match(/^(Unrealizable|Realizable)/);
  if (match) {
    return {
      result: match[1],
      resultType: capitalizedOnlyFirst(
        getMatchResFor_Combine01(reducedLines, match[1])
      ),
    };
  } else {
    return {
      result: "Stopped",
      resultType: "Stopped",
    };
  }
}

function process_lisa(data) {
  const match = data.match(/\n(UNREALIZABLE|REALIZABLE)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/UNREALIZABLE|REALIZABLE/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_nike(data) {
  const match = data.match(/(UNREALIZABLE|REALIZABLE)/);
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/UNREALIZABLE|REALIZABLE/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

function process_lydia(data) {
  const match = data.match(
    /\[\d{4}\-\d{2}\-\d{2} \d{2}:\d{2}:\d{2}\.\d+\] \[lydia\] \[info\] \[main\] (unrealizable|realizable)\./
  );
  if (match) {
    return {
      result: capitalizedOnlyFirst(
        match[0].match(/unrealizable|realizable/)[0]
      ),
    };
  } else {
    return {
      result: "Stopped",
    };
  }
}

const proces_funcs = {
  ltlfsyn: {
    just_res: process_ltlfsyn,
  },
  ltlfsynSyft: {
    just_res: process_ltlfsynSyft,
  },
  ltlfsynSyft_Cases: {
    just_res: process_ltlfsynSyft_Cases,
  },
  lydia: {
    just_res: process_lydia,
  },
  lisa: {
    just_res: process_lisa,
  },
  nike: {
    just_res: process_nike,
  },
  lisaComp: {
    just_res: process_nike,
  },
  lydiaComp: {
    just_res: process_nike,
  },
};

async function get_res(filePath, processFunc) {
  const { data } = await readFileAsString(filePath);
  if (data === null) {
    return {
      result: "NoResFile",
    };
  }
  if (data === "") {
    return {
      result: "EmptyResFile",
    };
  }
  // console.log(data);
  const synthesisResObj = processFunc(data);
  return {
    ...synthesisResObj,
    ...processTimeDetailInfo(data),
  }
}

module.exports = {
  readFileAsString,
  get_res,
  proces_funcs,
};
